i, j:, f:({i..j}). (n:{i..j}. 0  f(n))  0  i  n < j. f(n) 

latex

Definitions	P  Q, True, T, P  Q, , P & Q, i  j < k, x. t(x), t  T, x(s), P  Q, {i..j}, x:A. B(x), S  T
Lemmas	le int wf, ifthenelse wf, qmul zero qrng, qsum wf, int-rational, qsum-const2, rationals wf, true wf, squash wf, qle wf, le wf, int seg wf, int inc rationals, qsum-qle